<body>
<p>
Demonstrates an environmental control system for an office building
(<a href="http://www.cs.luc.edu/trull/latest/doc/javaws/office.jnlp">run this demo</a>).
</p>
<p>To introduce Trull and illustrate various features of Trull, we
describe an environmental control system for an office building. The design
of this system is compositional; aided by Trull constructs, the implementation
reflects this structure.
</p>
<p>We begin with the notion of an <i>office I/O</i>, which is a system
that accepts as input the events that control the environment of an office
(heating and lighting) and emits as output the various events necessary
to communicate with the rest of the environment-control system. Some of
these emitted events may originate from an action by a human occupant (switch
on/off, door open/close, and temperature request). The remaining output
event is a physical temperature reading, which may be automatically generated
from time to time. Office I/O illustrates the decoupling of system components
supported by Trull. The events emitted by an office I/O may be asynchronous
with the rest of the system. Furthermore, an office I/O may contain its
own autonomously evolving state--e.g., a process that controls how often
temperature readings are emitted based on how fast the temperature is changing.
</p>
<p>A <i>thermostat</i> partially automates the temperature control of an
office. An office I/O combined with a thermostat is called a
<i>temperature-stable office</i>. 
The pseudocode realization in Trull of these processes is
shown below, along with a diagram giving the interface of each process
in terms of the events that it emits and accepts. Note that some events
carry temperature data.
</p>
<pre> Thermostat:

   Temp actual_temp = INITIAL_ACTUAL_TEMP;
   Temp target_temp = INITIAL_TARGET_TEMP;

   loop
     await TEMP(t) -> 
             actual_temp = t;
             emit (t &lt; target_temp) ? HEATON : HEATOFF
         | SETTEMP(t) -> 
             target_temp = t;
             emit (actual_temp &lt; t) ? HEATON : HEATOFF

 Temperature_Stable_Office:

   Office_IO io;
   Thermostat therm;

   local HEATON HEATOFF TEMP in
     io || therm</pre>
<p>
The <tt>loop</tt> combinator in the thermostat implements an ``event loop'';
the body of the loop terminates after handling any event and restarts with
the next event. The body of the loop is a parallel composition (using the
<tt>||</tt> combinator) of two processes. The first process responds if
the current event is of the form <tt>TEMP(t)</tt> (a physical temperature
reading); on any other event, it terminates silently. It is similar for
the second process and events of form <tt>SETTEMP(t)</tt>. Thus, the body
of the loop is essentially a selection construct on the input events {
<tt>TEMP(t)</tt>, <tt>SETTEMP(t)</tt> }. In both parallel components, two
things happen on receipt of the specified event: an assignment takes place
and an event is emitted to control a heater. The assignment is an <i>action</i>,
written between braces, and may in general be any code in the host programming
language (typically something that terminates quickly). The <tt>emit</tt>
combinator emits an event. Events are delivered eventually (and simultaneously)
to all interested listeners and the emitting process terminates. Trull
thus distinguishes event emission from arbitrary Java actions.
</p>
<p>A thermostat is attached to an office I/O simply by composing them in
parallel, yielding a temperature-stable office process as illustrated above.
The parallel composition automatically ensures that the <tt>HEATON</tt>,
<tt>HEATOFF</tt>, and <tt>TEMP(t)</tt> events are transmitted between the
two subprocesses. In this case, these three events are hidden with the
<tt>local</tt> combinator so that they are not accessible externally as
either inputs or outputs, as shown in the diagram above.
</p>
<p>The occupant of an office should have manual control over the heat and
lights. This is done with the <i>occupant control</i> process that essentially
renames events.
</p>
<pre> Occupant_Control:

   loop
     await REQUESTTEMP(t) -> emit SETTEMP(t)
         | SWITCHON -> emit LIGHTON
         | SWITCHOFF -> emit LIGHTOFF</pre>
<p>Upon <tt>SWITCHON</tt>, the above process will eventually emit <tt>LIGHTON</tt>.
Trull makes no guarantee as to the timing of event emission, so it is
possible that <tt>SWITCHOFF</tt> could arrive <i>before</i> <tt>LIGHTON</tt>
is emitted and thus would not actually turn off the light. Later, we will
show a programming style to bulletproof against such cases. But in this
case, <tt>SWITCHON</tt> and <tt>SWITCHOFF</tt> originate from human actions,
and because we can reasonably assume that the light comes on faster than
a human can flip the switch, we would not expect the bad case ever to occur.
Trull supports a notion of ``<tt>assert</tt>'' statements appropriate
for concurrent programs, namely temporal-logic formulas, to express such
safety properties. These properties express the assumptions under which
a piece of Trull code functions correctly, in the spirit of preconditions
in Hoare-style rules for sequential programs. For instance, the formula
</p>
<pre>   LightOnPending =def ! LIGHTON since SWITCHON</pre>
<p>
expresses the property of a single point during an execution run that ``<tt>LIGHTON</tt>
did not occur since the most recent <tt>SWITCHON</tt>.'' Then, the formula
</p>
<pre>   SwOffSafety =def always (SWITCHOFF => ! LightOnPending)</pre>
<p>
expresses the property of an entire execution that ``whenever <tt>SWITCHOFF</tt>
occurs, there is no pending <tt>LIGHTON</tt>''. Adding <tt>SwOffSafety</tt>
(and the symmetric property for <tt>SWITCHON</tt>) to the office program
generates a run-time error whenever the property is violated. Similar properties
would be appropriate for the thermostat process.
</p>
<p>An office can be in two modes, <i>occupant mode</i> and <i>economy mode</i>.
Occupant mode is the normal mode of operation, as implemented by the occupant-control
process above. In economy mode, the temperature is reduced to and held
at a specified value, despite any requests otherwise, and the lights are
turned off and the switch disabled. The <tt>ECONOMYMODE(t)</tt> event puts
an office into economy mode, lowering the temperature to <tt>t</tt>, and
the <tt>OCCUPANTMODE</tt> event returns the office to occupant mode, restoring
the requested temperature to the most recent observed request. In addition,
if an office is in economy mode, it should temporarily revert to occupant
mode when the door is open, in case someone arrives in the middle of the
night to work; in that case, the office returns to economy mode when the
door is closed.
</p>
<p>The <i>economy control</i> process implements this control, emitting
<tt>SLEEP(t)</tt> whenever the office should enter economy mode, lowering
the temperature to <tt>t</tt>, and emitting <tt>AWAKE(t)</tt> whenever
the office should return to occupant mode, restoring the temperature to
<tt>t</tt>. The process runs three subprocesses in parallel. The first
one monitors continuously the last requested temperature (<tt>done</tt>
is the ``skip'' of Trull ; it does nothing and terminates immediately).
The second and third parallel components to determine when the office should
change modes. The code structure
</p>
<pre>   loop
     ECONOMYMODE(t) -> do
                         ...
                       watching OCCUPANTMODE
|| loop
     OCCUPANTMODE ->   do
                         ...
                       watching ECONOMYMODE</pre>
<p>
establishes mutual exclusion between the <i>occupant mode</i> and <i>economy
mode</i>. The invariant maintained is that the mode is determined by the
last occurrence of the events <tt>ECONOMYMODE</tt> and <tt>OCCUPANTMODE</tt>.
This structure also illustrates the technique of preempting a process to
establish priorities on events -- the events <tt>ECONOMYMODE</tt> and <tt>OCCUPANTMODE</tt>
have higher priority than the events occurring in the <tt>...</tt> above.
</p>
<p>On receipt of event <tt>ECONOMYMODE</tt>, a process enters a loop that
monitors the status of the office door. The invariant upon entry to the
loop is that the office has just been placed in economy mode and needs
to be put to sleep. While <tt>SLEEP</tt> is being emitted, the
<tt>await</tt>
combinator waits until <tt>DOOROPEN</tt> occurs. In the case that <tt>DOOROPEN</tt>
arrives while the emission of <tt>SLEEP</tt> is still pending, the emission
is aborted via the <tt>do/watching</tt> combinator to ensure consistency.
When the door becomes open, a symmetric process emits <tt>AWAKE</tt> and
waits for <tt>DOORCLOSE</tt>. On receipt of <tt>OCCUPANTMODE</tt>, the
door-monitoring loop is preempted and the office returns to occupant mode.
The code handles the possibility that <tt>ECONOMYMODE</tt> will arrive
while <tt>AWAKE</tt> is still pending.
</p>
<pre> Economy_Control:

   Temp last_temp = INITIAL_TARGET_TEMP;
   Temp economy;

      loop
        REQUESTTEMP(t) -> last_temp = t;
          done
   || loop
        ECONOMYMODE(t) -> economy = t;
          do
            loop
               do emit SLEEP(economy) watching DOOROPEN
            || await DOOROPEN ->
                        do emit AWAKE(last_temp) watching DOORCLOSE
                     || await DOORCLOSE -> done
          watching OCCUPANTMODE
   || loop
        await OCCUPANTMODE ->
                do emit AWAKE(last_temp) watching ECONOMYMODE</pre>
<p>
Now we build an <i>office control</i> process from an occupant-control
process and an economy-control process. Note that the occupant-control
process must be disabled during economy mode. This is done with the <tt>suspend/resume</tt>
combinator, which suspends a process on receipt of a specified event (<tt>SLEEP</tt>
in this case) and resumes it on another event (<tt>AWAKE</tt> in this case).
Thus, whenever the economy control sends a <tt>SLEEP</tt> event, the occupant
will lose control of the light and heat until the economy control sends
an <tt>AWAKE</tt> event. Two processes (not shown in the picture) run in
parallel with the occupant control and the economy control to adjust the
light and heat appropriately whenever the office toggles modes; each preempts
the other to avoid inconsistency. Note that parallel composition automatically
routes <tt>REQUESTTEMP(t)</tt> events to both subprocesses that accept
them.
</p>
<pre> Office_Control:

   Occupant_Control oc;
   Economy_Control ec;

   local SLEEP AWAKE in
      ec
   || suspend SLEEP resume AWAKE in oc
   || loop
        await SLEEP(t) -> 
           do 
              emit SETTEMP(t)
           || emit LIGHTOFF
           watching AWAKE
   || loop
        await AWAKE(t) -> 
           do 
              emit SETTEMP(t)
           watching SLEEP</pre>
<p>
The office control is rather complex, and so we may want to sprinkle in
some temporal safety properties to be checked during execution. For instance,
using definitions
</p>
<pre>     Slp =def ! AWAKE since SLEEP
     Awk =def (! SLEEP since AWAKE) \/ always (! SLEEP)
    SwOn =def ! SWITCHOFF since SWITCHON
   SwOff =def ! SWITCHON since SWITCHOFF</pre>
<p>
where <tt>always (! SLEEP)</tt> means that <tt>SLEEP</tt> never occurred
(i.e., an office is initially awake), we define the following property
to specify the behavior of the light:
</p>
<pre>   LightSafety =def always (  (LIGHTON  => Awk /\ SwOn)
                           \/ (LIGHTOFF => Slp \/ SwOff))</pre>
<p>
This specifies that whenever <tt>LIGHTON</tt> occurs, both the office must
be awake (no <tt>SLEEP</tt> since the last <tt>AWAKE</tt>) and the switch
must be on (defined similarly). Also, whenever LightOff occurs, either
the office must be asleep or the switch must be off. Note that <tt>SLEEP
xor AWAKE</tt> is a tautology, but that this is not quite true of
<tt>SwOn
xor SwOff</tt> because neither <tt>SwOn</tt> nor <tt>SwOff</tt> is true
during an execution until the first <tt>SWITCHON</tt> or <tt>SWITCHOFF</tt>
event.
</p>
<p>To complete the implementation of a single office, we compose a temperature-stable
office with an office control. The resulting
<i>office</i> process emits
no events and accepts only events <tt>ECONOMYMODE(t)</tt> and <tt>OCCUPANTMODE</tt>.
The <tt>local</tt> combinator hides all other events.
</p>
<pre> Office:

   Temperature_Stable_Office tso;
   Office_Control oc;

   local SWITCHON SWITCHOFF LIGHTON LIGHTOFF
         REQUESTTEMP SETTEMP DOOROPEN DOORCLOSE
   in 
     tso || oc</pre>
<p>
Finally, multiple offices are combined into an entire floor of an office
building. The implementation below allows offices to be added one by one.
The entire floor is commanded to be placed in economy mode and to be restored
to occupant mode as a whole. However, while in economy mode, individual
offices may temporarily revert to occupant mode due to door activity, as
described above.
</p>
<pre> Building_Floor:

   Building_Floor bf;
   Office o;

   bf || o</pre>
<p>
We conclude this example by recalling our earlier comments about asynchronous
communication. In a building with many offices, each office is mostly decoupled
from the others. Logically, the only communication shared between them
is the <tt>ECONOMYMODE(t)</tt> and <tt>OCCUPANTMODE</tt> events. Furthermore,
each office I/O typically generates events asynchronously with the other
offices. Trull supports this kind of decoupling, allowing each office
to evolve autonomously of the others.
</p>
</body>